Nuprl Lemma : divides_preorder
2,24
postcript
pdf
Preorder(
;
x
,
y
.
x
|
y
)
latex
Definitions
Preorder(
T
;
x
,
y
.
R
(
x
;
y
))
,
Refl(
T
;
x
,
y
.
E
(
x
;
y
))
,
Trans
x
,
y
:
T
.
E
(
x
;
y
)
,
P
&
Q
,
P
Q
,
b
|
a
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
divides
transitivity
,
divides
reflexivity
,
divides
wf
origin
;x,y.x | y) ;x,y.x | y) 
Q
x:A. B(x)
T